FDL - Step of Proof: inv_image_ind

Step of Proof: inv_image_ind_a

9,38

Inference at * 1
Iof proof for Lemma inv image ind a:

1. T : Type
2. r : T

3. S : Type
4. f : S

T
5. WellFnd{i}(T;x,y.r(x,y))

WellFnd{i}(S;x,y.r(f(x),f(y)))

by ((((RepUnfolds ``wellfounded guard`` 0)

CollapseTHEN (RepD))

)

CollapseTHENA (

C(Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t) inil_term)))

C1:

C1: 6. P : S

C1: 7.

j:S. (

k:S. r(f(k),f(j))

P(k))

P(j)

C1: 8. n : S

C1:

P(n)

Definitions t T, {T}, x(s), P Q, x:A. B(x), x(s1,s2), WellFnd{i}(A;x,y.R(x;y)),